(1
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 137)
  ("(var3 stable)" 137 220)
  ("(var3 up)" 220 223)
  ("(var3 down)" 223 232)
  ("(var3 up)" 232 238)
  ("(var3 stable)" 238 381)
  ("(var4 stable)" 0 101)
  ("(var4 up)" 101 127)
  ("(var4 stable)" 127 232)
  ("(var4 down)" 232 347)
  ("(var4 stable)" 347 381)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 99)
  ("(var1 up)" 99 101)
  ("(var1 stable)" 101 103)
  ("(var1 up)" 103 126)
  ("(var1 stable)" 126 381)
  ("(var2 stable)" 0 116)
  ("(var2 down)" 116 124)
  ("(var2 up)" 124 264)
  ("(var2 stable)" 264 381)
 )
)
(2
 (
  ("(var3 stable)" 0 100)
  ("(var3 up)" 100 128)
  ("(var3 stable)" 128 215)
  ("(var3 up)" 215 220)
  ("(var3 down)" 220 232)
  ("(var3 up)" 232 239)
  ("(var3 stable)" 239 378)
  ("(var4 stable)" 0 100)
  ("(var4 up)" 100 127)
  ("(var4 stable)" 127 249)
  ("(var4 down)" 249 355)
  ("(var4 stable)" 355 378)
  ("(var1 stable)" 0 98)
  ("(var1 up)" 98 130)
  ("(var1 stable)" 130 378)
  ("(var2 stable)" 0 117)
  ("(var2 down)" 117 119)
  ("(var2 up)" 119 252)
  ("(var2 stable)" 252 378)
 )
)
(3
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 75)
  ("(var3 stable)" 75 155)
  ("(var3 up)" 155 158)
  ("(var3 down)" 158 169)
  ("(var3 up)" 169 174)
  ("(var3 stable)" 174 303)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 82)
  ("(var4 stable)" 82 165)
  ("(var4 down)" 165 199)
  ("(var4 stable)" 199 201)
  ("(var4 down)" 201 274)
  ("(var4 stable)" 274 303)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 73)
  ("(var1 stable)" 73 303)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 68)
  ("(var2 up)" 68 186)
  ("(var2 stable)" 186 303)
 )
)
(4
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 76)
  ("(var3 stable)" 76 162)
  ("(var3 up)" 162 168)
  ("(var3 down)" 168 179)
  ("(var3 up)" 179 185)
  ("(var3 stable)" 185 325)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 76)
  ("(var4 stable)" 76 192)
  ("(var4 down)" 192 279)
  ("(var4 stable)" 279 325)
  ("(var1 stable)" 0 41)
  ("(var1 down)" 41 43)
  ("(var1 up)" 43 57)
  ("(var1 down)" 57 59)
  ("(var1 up)" 59 83)
  ("(var1 stable)" 83 325)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 68)
  ("(var2 stable)" 68 110)
  ("(var2 up)" 110 194)
  ("(var2 down)" 194 196)
  ("(var2 up)" 196 198)
  ("(var2 stable)" 198 325)
 )
)
(5
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 44)
  ("(var3 stable)" 44 46)
  ("(var3 up)" 46 54)
  ("(var3 stable)" 54 56)
  ("(var3 up)" 56 78)
  ("(var3 stable)" 78 162)
  ("(var3 up)" 162 169)
  ("(var3 down)" 169 181)
  ("(var3 up)" 181 186)
  ("(var3 stable)" 186 326)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 43)
  ("(var4 down)" 43 46)
  ("(var4 up)" 46 74)
  ("(var4 down)" 74 76)
  ("(var4 up)" 76 81)
  ("(var4 stable)" 81 207)
  ("(var4 down)" 207 282)
  ("(var4 stable)" 282 326)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 75)
  ("(var1 stable)" 75 326)
  ("(var2 stable)" 0 64)
  ("(var2 down)" 64 66)
  ("(var2 stable)" 66 107)
  ("(var2 up)" 107 175)
  ("(var2 down)" 175 177)
  ("(var2 up)" 177 213)
  ("(var2 stable)" 213 326)
 )
)
(6
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 97)
  ("(var3 stable)" 97 174)
  ("(var3 up)" 174 178)
  ("(var3 down)" 178 188)
  ("(var3 up)" 188 194)
  ("(var3 stable)" 194 323)
  ("(var4 stable)" 0 66)
  ("(var4 down)" 66 68)
  ("(var4 up)" 68 89)
  ("(var4 stable)" 89 91)
  ("(var4 up)" 91 94)
  ("(var4 stable)" 94 186)
  ("(var4 down)" 186 274)
  ("(var4 stable)" 274 323)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 95)
  ("(var1 stable)" 95 323)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 87)
  ("(var2 up)" 87 209)
  ("(var2 stable)" 209 323)
 )
)
(7
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 96)
  ("(var3 stable)" 96 170)
  ("(var3 up)" 170 176)
  ("(var3 down)" 176 183)
  ("(var3 up)" 183 187)
  ("(var3 stable)" 187 315)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 101)
  ("(var4 stable)" 101 183)
  ("(var4 down)" 183 280)
  ("(var4 stable)" 280 315)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 91)
  ("(var1 stable)" 91 315)
  ("(var2 stable)" 0 87)
  ("(var2 down)" 87 89)
  ("(var2 up)" 89 124)
  ("(var2 down)" 124 126)
  ("(var2 up)" 126 212)
  ("(var2 stable)" 212 315)
 )
)
(8
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 98)
  ("(var3 stable)" 98 183)
  ("(var3 up)" 183 187)
  ("(var3 down)" 187 197)
  ("(var3 up)" 197 203)
  ("(var3 stable)" 203 351)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 98)
  ("(var4 stable)" 98 214)
  ("(var4 down)" 214 216)
  ("(var4 stable)" 216 219)
  ("(var4 up)" 219 221)
  ("(var4 down)" 221 303)
  ("(var4 stable)" 303 351)
  ("(var1 stable)" 0 66)
  ("(var1 down)" 66 68)
  ("(var1 up)" 68 96)
  ("(var1 stable)" 96 351)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 up)" 85 223)
  ("(var2 down)" 223 225)
  ("(var2 up)" 225 227)
  ("(var2 stable)" 227 351)
 )
)
(9
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 97)
  ("(var3 stable)" 97 181)
  ("(var3 down)" 181 183)
  ("(var3 up)" 183 188)
  ("(var3 down)" 188 198)
  ("(var3 up)" 198 204)
  ("(var3 stable)" 204 346)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 96)
  ("(var4 stable)" 96 202)
  ("(var4 down)" 202 298)
  ("(var4 stable)" 298 300)
  ("(var4 down)" 300 309)
  ("(var4 stable)" 309 346)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 89)
  ("(var1 stable)" 89 346)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 87)
  ("(var2 stable)" 87 120)
  ("(var2 up)" 120 224)
  ("(var2 stable)" 224 346)
 )
)
(10
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 113)
  ("(var3 stable)" 113 116)
  ("(var3 up)" 116 118)
  ("(var3 stable)" 118 196)
  ("(var3 up)" 196 200)
  ("(var3 stable)" 200 203)
  ("(var3 down)" 203 212)
  ("(var3 up)" 212 217)
  ("(var3 stable)" 217 356)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 124)
  ("(var4 stable)" 124 219)
  ("(var4 down)" 219 312)
  ("(var4 stable)" 312 354)
  ("(var4 up)" 354 356)
  ("(var1 stable)" 0 87)
  ("(var1 down)" 87 89)
  ("(var1 up)" 89 116)
  ("(var1 stable)" 116 356)
  ("(var2 stable)" 0 103)
  ("(var2 down)" 103 105)
  ("(var2 up)" 105 240)
  ("(var2 stable)" 240 356)
 )
)
(11
 (
  ("(var3 stable)" 0 28)
  ("(var3 up)" 28 65)
  ("(var3 down)" 65 67)
  ("(var3 up)" 67 69)
  ("(var3 stable)" 69 146)
  ("(var3 up)" 146 151)
  ("(var3 down)" 151 160)
  ("(var3 up)" 160 167)
  ("(var3 stable)" 167 293)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 72)
  ("(var4 stable)" 72 156)
  ("(var4 down)" 156 246)
  ("(var4 stable)" 246 293)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 63)
  ("(var1 stable)" 63 293)
  ("(var2 stable)" 0 58)
  ("(var2 up)" 58 196)
  ("(var2 stable)" 196 291)
  ("(var2 down)" 291 293)
 )
)
(12
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 81)
  ("(var3 stable)" 81 170)
  ("(var3 up)" 170 174)
  ("(var3 down)" 174 185)
  ("(var3 up)" 185 192)
  ("(var3 stable)" 192 334)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 41)
  ("(var4 down)" 41 44)
  ("(var4 up)" 44 90)
  ("(var4 stable)" 90 186)
  ("(var4 down)" 186 289)
  ("(var4 stable)" 289 332)
  ("(var4 up)" 332 334)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 78)
  ("(var1 stable)" 78 334)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 207)
  ("(var2 stable)" 207 334)
 )
)
(13
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 96)
  ("(var3 stable)" 96 98)
  ("(var3 up)" 98 100)
  ("(var3 stable)" 100 176)
  ("(var3 up)" 176 182)
  ("(var3 down)" 182 192)
  ("(var3 up)" 192 197)
  ("(var3 stable)" 197 341)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 98)
  ("(var4 stable)" 98 218)
  ("(var4 down)" 218 297)
  ("(var4 stable)" 297 341)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 89)
  ("(var1 stable)" 89 341)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 84)
  ("(var2 stable)" 84 124)
  ("(var2 up)" 124 185)
  ("(var2 stable)" 185 187)
  ("(var2 up)" 187 224)
  ("(var2 stable)" 224 341)
 )
)
(14
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 87)
  ("(var3 stable)" 87 163)
  ("(var3 up)" 163 168)
  ("(var3 down)" 168 177)
  ("(var3 up)" 177 182)
  ("(var3 stable)" 182 308)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 92)
  ("(var4 stable)" 92 179)
  ("(var4 down)" 179 182)
  ("(var4 up)" 182 184)
  ("(var4 down)" 184 252)
  ("(var4 stable)" 252 256)
  ("(var4 down)" 256 280)
  ("(var4 stable)" 280 308)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 85)
  ("(var1 stable)" 85 308)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 179)
  ("(var2 stable)" 179 308)
 )
)
(15
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 110)
  ("(var3 down)" 110 112)
  ("(var3 stable)" 112 182)
  ("(var3 up)" 182 186)
  ("(var3 stable)" 186 188)
  ("(var3 down)" 188 194)
  ("(var3 up)" 194 198)
  ("(var3 stable)" 198 331)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 112)
  ("(var4 stable)" 112 193)
  ("(var4 down)" 193 299)
  ("(var4 stable)" 299 331)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 102)
  ("(var1 stable)" 102 331)
  ("(var2 stable)" 0 99)
  ("(var2 down)" 99 101)
  ("(var2 stable)" 101 134)
  ("(var2 up)" 134 193)
  ("(var2 down)" 193 195)
  ("(var2 up)" 195 226)
  ("(var2 stable)" 226 331)
 )
)
(16
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 108)
  ("(var3 down)" 108 110)
  ("(var3 stable)" 110 186)
  ("(var3 up)" 186 190)
  ("(var3 stable)" 190 192)
  ("(var3 down)" 192 201)
  ("(var3 up)" 201 207)
  ("(var3 stable)" 207 339)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 108)
  ("(var4 stable)" 108 207)
  ("(var4 down)" 207 293)
  ("(var4 stable)" 293 337)
  ("(var4 up)" 337 339)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 103)
  ("(var1 stable)" 103 339)
  ("(var2 stable)" 0 128)
  ("(var2 up)" 128 213)
  ("(var2 stable)" 213 216)
  ("(var2 up)" 216 218)
  ("(var2 stable)" 218 339)
 )
)
(17
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 71)
  ("(var3 stable)" 71 73)
  ("(var3 up)" 73 75)
  ("(var3 stable)" 75 154)
  ("(var3 up)" 154 160)
  ("(var3 down)" 160 169)
  ("(var3 up)" 169 174)
  ("(var3 stable)" 174 311)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 75)
  ("(var4 stable)" 75 165)
  ("(var4 up)" 165 167)
  ("(var4 down)" 167 262)
  ("(var4 stable)" 262 311)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 68)
  ("(var1 stable)" 68 311)
  ("(var2 stable)" 0 62)
  ("(var2 down)" 62 64)
  ("(var2 stable)" 64 99)
  ("(var2 up)" 99 101)
  ("(var2 stable)" 101 103)
  ("(var2 up)" 103 159)
  ("(var2 stable)" 159 161)
  ("(var2 up)" 161 206)
  ("(var2 stable)" 206 311)
 )
)
(18
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 76)
  ("(var3 stable)" 76 156)
  ("(var3 up)" 156 159)
  ("(var3 down)" 159 170)
  ("(var3 up)" 170 176)
  ("(var3 stable)" 176 306)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 78)
  ("(var4 stable)" 78 166)
  ("(var4 down)" 166 265)
  ("(var4 stable)" 265 306)
  ("(var1 stable)" 0 45)
  ("(var1 up)" 45 71)
  ("(var1 stable)" 71 306)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 68)
  ("(var2 stable)" 68 103)
  ("(var2 up)" 103 196)
  ("(var2 down)" 196 199)
  ("(var2 up)" 199 201)
  ("(var2 stable)" 201 306)
 )
)
(19
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 106)
  ("(var3 stable)" 106 193)
  ("(var3 up)" 193 197)
  ("(var3 down)" 197 207)
  ("(var3 stable)" 207 209)
  ("(var3 up)" 209 215)
  ("(var3 stable)" 215 352)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 106)
  ("(var4 stable)" 106 238)
  ("(var4 down)" 238 309)
  ("(var4 up)" 309 312)
  ("(var4 down)" 312 315)
  ("(var4 stable)" 315 352)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 102)
  ("(var1 stable)" 102 352)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 up)" 98 240)
  ("(var2 stable)" 240 352)
 )
)
(20
 (
  ("(var3 stable)" 0 63)
  ("(var3 down)" 63 65)
  ("(var3 up)" 65 85)
  ("(var3 down)" 85 87)
  ("(var3 up)" 87 90)
  ("(var3 stable)" 90 164)
  ("(var3 up)" 164 170)
  ("(var3 down)" 170 178)
  ("(var3 up)" 178 182)
  ("(var3 stable)" 182 314)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 94)
  ("(var4 stable)" 94 168)
  ("(var4 down)" 168 263)
  ("(var4 up)" 263 265)
  ("(var4 down)" 265 270)
  ("(var4 stable)" 270 314)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 66)
  ("(var1 down)" 66 68)
  ("(var1 up)" 68 86)
  ("(var1 stable)" 86 314)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 199)
  ("(var2 stable)" 199 314)
 )
)
(21
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 73)
  ("(var3 stable)" 73 75)
  ("(var3 up)" 75 105)
  ("(var3 stable)" 105 188)
  ("(var3 up)" 188 192)
  ("(var3 down)" 192 204)
  ("(var3 up)" 204 208)
  ("(var3 stable)" 208 347)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 105)
  ("(var4 stable)" 105 234)
  ("(var4 down)" 234 298)
  ("(var4 stable)" 298 300)
  ("(var4 down)" 300 302)
  ("(var4 stable)" 302 347)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 97)
  ("(var1 down)" 97 99)
  ("(var1 up)" 99 101)
  ("(var1 stable)" 101 347)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 up)" 94 199)
  ("(var2 down)" 199 203)
  ("(var2 up)" 203 237)
  ("(var2 stable)" 237 347)
 )
)
(22
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 116)
  ("(var3 stable)" 116 203)
  ("(var3 up)" 203 207)
  ("(var3 down)" 207 216)
  ("(var3 stable)" 216 218)
  ("(var3 up)" 218 222)
  ("(var3 stable)" 222 361)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 117)
  ("(var4 stable)" 117 215)
  ("(var4 down)" 215 324)
  ("(var4 up)" 324 326)
  ("(var4 down)" 326 330)
  ("(var4 stable)" 330 361)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 90)
  ("(var1 down)" 90 92)
  ("(var1 up)" 92 117)
  ("(var1 stable)" 117 361)
  ("(var2 stable)" 0 106)
  ("(var2 down)" 106 108)
  ("(var2 up)" 108 239)
  ("(var2 down)" 239 241)
  ("(var2 stable)" 241 361)
 )
)
(23
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 88)
  ("(var3 stable)" 88 161)
  ("(var3 up)" 161 165)
  ("(var3 down)" 165 175)
  ("(var3 up)" 175 180)
  ("(var3 stable)" 180 313)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 84)
  ("(var4 stable)" 84 197)
  ("(var4 down)" 197 259)
  ("(var4 stable)" 259 261)
  ("(var4 down)" 261 263)
  ("(var4 stable)" 263 313)
  ("(var1 stable)" 0 2)
  ("(var1 down)" 2 4)
  ("(var1 stable)" 4 48)
  ("(var1 up)" 48 76)
  ("(var1 stable)" 76 313)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 213)
  ("(var2 stable)" 213 313)
 )
)
(24
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 108)
  ("(var3 stable)" 108 187)
  ("(var3 up)" 187 191)
  ("(var3 down)" 191 201)
  ("(var3 up)" 201 205)
  ("(var3 stable)" 205 333)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 111)
  ("(var4 stable)" 111 200)
  ("(var4 down)" 200 300)
  ("(var4 stable)" 300 333)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 106)
  ("(var1 down)" 106 108)
  ("(var1 stable)" 108 333)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 102)
  ("(var2 up)" 102 131)
  ("(var2 down)" 131 133)
  ("(var2 up)" 133 227)
  ("(var2 stable)" 227 333)
 )
)
(25
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 96)
  ("(var3 stable)" 96 163)
  ("(var3 up)" 163 169)
  ("(var3 down)" 169 176)
  ("(var3 up)" 176 181)
  ("(var3 stable)" 181 310)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 88)
  ("(var4 stable)" 88 170)
  ("(var4 down)" 170 268)
  ("(var4 stable)" 268 310)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 58)
  ("(var1 up)" 58 83)
  ("(var1 stable)" 83 310)
  ("(var2 stable)" 0 75)
  ("(var2 down)" 75 77)
  ("(var2 up)" 77 195)
  ("(var2 stable)" 195 310)
 )
)
(26
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 87)
  ("(var3 stable)" 87 177)
  ("(var3 up)" 177 181)
  ("(var3 down)" 181 192)
  ("(var3 up)" 192 197)
  ("(var3 stable)" 197 348)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 93)
  ("(var4 stable)" 93 221)
  ("(var4 down)" 221 226)
  ("(var4 up)" 226 228)
  ("(var4 down)" 228 298)
  ("(var4 up)" 298 300)
  ("(var4 down)" 300 302)
  ("(var4 stable)" 302 348)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 82)
  ("(var1 stable)" 82 348)
  ("(var2 stable)" 0 76)
  ("(var2 down)" 76 80)
  ("(var2 stable)" 80 116)
  ("(var2 up)" 116 193)
  ("(var2 stable)" 193 197)
  ("(var2 up)" 197 199)
  ("(var2 stable)" 199 226)
  ("(var2 down)" 226 228)
  ("(var2 stable)" 228 348)
 )
)
(27
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 87)
  ("(var3 down)" 87 89)
  ("(var3 up)" 89 91)
  ("(var3 stable)" 91 168)
  ("(var3 up)" 168 173)
  ("(var3 down)" 173 183)
  ("(var3 up)" 183 189)
  ("(var3 stable)" 189 323)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 99)
  ("(var4 stable)" 99 178)
  ("(var4 down)" 178 275)
  ("(var4 stable)" 275 278)
  ("(var4 down)" 278 280)
  ("(var4 stable)" 280 323)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 92)
  ("(var1 stable)" 92 323)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 204)
  ("(var2 stable)" 204 323)
 )
)
(28
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 81)
  ("(var3 stable)" 81 153)
  ("(var3 up)" 153 159)
  ("(var3 down)" 159 169)
  ("(var3 up)" 169 174)
  ("(var3 stable)" 174 302)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 50)
  ("(var4 up)" 50 82)
  ("(var4 stable)" 82 154)
  ("(var4 down)" 154 156)
  ("(var4 up)" 156 158)
  ("(var4 stable)" 158 186)
  ("(var4 down)" 186 252)
  ("(var4 stable)" 252 254)
  ("(var4 down)" 254 256)
  ("(var4 stable)" 256 300)
  ("(var4 up)" 300 302)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 82)
  ("(var1 stable)" 82 302)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 199)
  ("(var2 stable)" 199 302)
 )
)
(29
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 85)
  ("(var3 down)" 85 87)
  ("(var3 stable)" 87 170)
  ("(var3 up)" 170 176)
  ("(var3 down)" 176 186)
  ("(var3 up)" 186 192)
  ("(var3 stable)" 192 334)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 92)
  ("(var4 stable)" 92 189)
  ("(var4 down)" 189 304)
  ("(var4 stable)" 304 334)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 84)
  ("(var1 stable)" 84 334)
  ("(var2 stable)" 0 74)
  ("(var2 down)" 74 78)
  ("(var2 up)" 78 166)
  ("(var2 stable)" 166 168)
  ("(var2 up)" 168 170)
  ("(var2 down)" 170 172)
  ("(var2 up)" 172 210)
  ("(var2 down)" 210 212)
  ("(var2 up)" 212 216)
  ("(var2 down)" 216 218)
  ("(var2 up)" 218 220)
  ("(var2 stable)" 220 334)
 )
)
(30
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 61)
  ("(var3 down)" 61 63)
  ("(var3 stable)" 63 142)
  ("(var3 up)" 142 146)
  ("(var3 down)" 146 156)
  ("(var3 up)" 156 163)
  ("(var3 stable)" 163 286)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 67)
  ("(var4 stable)" 67 169)
  ("(var4 down)" 169 171)
  ("(var4 stable)" 171 177)
  ("(var4 down)" 177 256)
  ("(var4 stable)" 256 286)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 62)
  ("(var1 stable)" 62 286)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 up)" 55 97)
  ("(var2 stable)" 97 99)
  ("(var2 up)" 99 169)
  ("(var2 stable)" 169 286)
 )
)
(31
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 91)
  ("(var3 stable)" 91 181)
  ("(var3 up)" 181 186)
  ("(var3 down)" 186 195)
  ("(var3 stable)" 195 197)
  ("(var3 up)" 197 200)
  ("(var3 stable)" 200 351)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 104)
  ("(var4 stable)" 104 193)
  ("(var4 down)" 193 308)
  ("(var4 up)" 308 311)
  ("(var4 stable)" 311 351)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 94)
  ("(var1 stable)" 94 351)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 227)
  ("(var2 stable)" 227 351)
 )
)
(32
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 83)
  ("(var3 stable)" 83 154)
  ("(var3 up)" 154 161)
  ("(var3 down)" 161 172)
  ("(var3 up)" 172 174)
  ("(var3 stable)" 174 305)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 84)
  ("(var4 stable)" 84 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 166)
  ("(var4 down)" 166 260)
  ("(var4 stable)" 260 305)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 77)
  ("(var1 stable)" 77 305)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 207)
  ("(var2 stable)" 207 305)
 )
)
(33
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 109)
  ("(var3 stable)" 109 191)
  ("(var3 up)" 191 196)
  ("(var3 down)" 196 206)
  ("(var3 up)" 206 211)
  ("(var3 stable)" 211 345)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 112)
  ("(var4 stable)" 112 209)
  ("(var4 down)" 209 305)
  ("(var4 stable)" 305 341)
  ("(var4 up)" 341 343)
  ("(var4 down)" 343 345)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 104)
  ("(var1 stable)" 104 345)
  ("(var2 stable)" 0 100)
  ("(var2 down)" 100 102)
  ("(var2 up)" 102 221)
  ("(var2 stable)" 221 345)
 )
)
(34
 (
  ("(var3 stable)" 0 27)
  ("(var3 up)" 27 64)
  ("(var3 stable)" 64 136)
  ("(var3 up)" 136 139)
  ("(var3 down)" 139 149)
  ("(var3 up)" 149 154)
  ("(var3 stable)" 154 275)
  ("(var4 stable)" 0 27)
  ("(var4 up)" 27 57)
  ("(var4 stable)" 57 59)
  ("(var4 up)" 59 62)
  ("(var4 stable)" 62 168)
  ("(var4 down)" 168 235)
  ("(var4 stable)" 235 275)
  ("(var1 stable)" 0 31)
  ("(var1 up)" 31 59)
  ("(var1 stable)" 59 275)
  ("(var2 stable)" 0 51)
  ("(var2 down)" 51 53)
  ("(var2 up)" 53 172)
  ("(var2 down)" 172 174)
  ("(var2 up)" 174 176)
  ("(var2 stable)" 176 275)
 )
)
(35
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 112)
  ("(var3 stable)" 112 181)
  ("(var3 up)" 181 186)
  ("(var3 down)" 186 195)
  ("(var3 up)" 195 200)
  ("(var3 stable)" 200 329)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 110)
  ("(var4 stable)" 110 188)
  ("(var4 down)" 188 190)
  ("(var4 up)" 190 192)
  ("(var4 down)" 192 286)
  ("(var4 up)" 286 288)
  ("(var4 stable)" 288 329)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 78)
  ("(var1 down)" 78 80)
  ("(var1 up)" 80 100)
  ("(var1 stable)" 100 329)
  ("(var2 stable)" 0 94)
  ("(var2 down)" 94 96)
  ("(var2 up)" 96 204)
  ("(var2 stable)" 204 329)
 )
)
(36
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 100)
  ("(var3 down)" 100 102)
  ("(var3 up)" 102 106)
  ("(var3 stable)" 106 181)
  ("(var3 up)" 181 183)
  ("(var3 down)" 183 193)
  ("(var3 up)" 193 197)
  ("(var3 stable)" 197 326)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 104)
  ("(var4 down)" 104 106)
  ("(var4 stable)" 106 202)
  ("(var4 up)" 202 204)
  ("(var4 down)" 204 299)
  ("(var4 stable)" 299 326)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 97)
  ("(var1 stable)" 97 326)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 stable)" 94 126)
  ("(var2 up)" 126 216)
  ("(var2 down)" 216 218)
  ("(var2 stable)" 218 326)
 )
)
(37
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 106)
  ("(var3 stable)" 106 182)
  ("(var3 up)" 182 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 201)
  ("(var3 stable)" 201 331)
  ("(var4 stable)" 0 71)
  ("(var4 down)" 71 73)
  ("(var4 up)" 73 103)
  ("(var4 stable)" 103 105)
  ("(var4 up)" 105 108)
  ("(var4 stable)" 108 204)
  ("(var4 down)" 204 302)
  ("(var4 stable)" 302 331)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 100)
  ("(var1 stable)" 100 331)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 96)
  ("(var2 stable)" 96 119)
  ("(var2 up)" 119 133)
  ("(var2 down)" 133 135)
  ("(var2 up)" 135 224)
  ("(var2 stable)" 224 331)
 )
)
(38
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 87)
  ("(var3 stable)" 87 164)
  ("(var3 up)" 164 172)
  ("(var3 stable)" 172 174)
  ("(var3 down)" 174 184)
  ("(var3 up)" 184 188)
  ("(var3 stable)" 188 329)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 72)
  ("(var4 stable)" 72 74)
  ("(var4 up)" 74 79)
  ("(var4 stable)" 79 177)
  ("(var4 down)" 177 286)
  ("(var4 stable)" 286 329)
  ("(var1 up)" 0 5)
  ("(var1 down)" 5 7)
  ("(var1 stable)" 7 44)
  ("(var1 up)" 44 46)
  ("(var1 down)" 46 48)
  ("(var1 up)" 48 75)
  ("(var1 stable)" 75 329)
  ("(var2 stable)" 0 63)
  ("(var2 down)" 63 67)
  ("(var2 stable)" 67 109)
  ("(var2 up)" 109 205)
  ("(var2 stable)" 205 329)
 )
)
(39
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 54)
  ("(var3 down)" 54 57)
  ("(var3 up)" 57 103)
  ("(var3 stable)" 103 161)
  ("(var3 up)" 161 167)
  ("(var3 stable)" 167 169)
  ("(var3 down)" 169 178)
  ("(var3 up)" 178 183)
  ("(var3 stable)" 183 311)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 94)
  ("(var4 stable)" 94 177)
  ("(var4 down)" 177 180)
  ("(var4 up)" 180 182)
  ("(var4 down)" 182 283)
  ("(var4 stable)" 283 311)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 91)
  ("(var1 stable)" 91 311)
  ("(var2 stable)" 0 77)
  ("(var2 down)" 77 79)
  ("(var2 up)" 79 204)
  ("(var2 stable)" 204 311)
 )
)
(40
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 91)
  ("(var3 stable)" 91 169)
  ("(var3 up)" 169 173)
  ("(var3 down)" 173 184)
  ("(var3 up)" 184 188)
  ("(var3 stable)" 188 322)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 87)
  ("(var4 stable)" 87 178)
  ("(var4 up)" 178 180)
  ("(var4 down)" 180 278)
  ("(var4 stable)" 278 322)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 90)
  ("(var1 stable)" 90 322)
  ("(var2 stable)" 0 77)
  ("(var2 down)" 77 79)
  ("(var2 up)" 79 123)
  ("(var2 stable)" 123 126)
  ("(var2 up)" 126 204)
  ("(var2 stable)" 204 322)
 )
)
(41
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 103)
  ("(var3 stable)" 103 105)
  ("(var3 up)" 105 107)
  ("(var3 stable)" 107 182)
  ("(var3 up)" 182 187)
  ("(var3 down)" 187 196)
  ("(var3 up)" 196 203)
  ("(var3 stable)" 203 331)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 107)
  ("(var4 stable)" 107 215)
  ("(var4 down)" 215 304)
  ("(var4 stable)" 304 331)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 96)
  ("(var1 down)" 96 98)
  ("(var1 stable)" 98 331)
  ("(var2 stable)" 0 91)
  ("(var2 down)" 91 95)
  ("(var2 up)" 95 133)
  ("(var2 down)" 133 135)
  ("(var2 up)" 135 228)
  ("(var2 stable)" 228 331)
 )
)
(42
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 63)
  ("(var3 up)" 63 98)
  ("(var3 stable)" 98 186)
  ("(var3 up)" 186 188)
  ("(var3 stable)" 188 191)
  ("(var3 down)" 191 201)
  ("(var3 up)" 201 205)
  ("(var3 stable)" 205 351)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 95)
  ("(var4 stable)" 95 199)
  ("(var4 down)" 199 304)
  ("(var4 up)" 304 306)
  ("(var4 down)" 306 308)
  ("(var4 stable)" 308 343)
  ("(var4 down)" 343 345)
  ("(var4 stable)" 345 351)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 91)
  ("(var1 down)" 91 93)
  ("(var1 stable)" 93 351)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 up)" 85 218)
  ("(var2 down)" 218 221)
  ("(var2 stable)" 221 351)
 )
)
(43
 (
  ("(var3 stable)" 0 41)
  ("(var3 down)" 41 43)
  ("(var3 up)" 43 73)
  ("(var3 stable)" 73 75)
  ("(var3 up)" 75 77)
  ("(var3 stable)" 77 150)
  ("(var3 up)" 150 154)
  ("(var3 stable)" 154 156)
  ("(var3 down)" 156 164)
  ("(var3 up)" 164 169)
  ("(var3 stable)" 169 290)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 78)
  ("(var4 stable)" 78 191)
  ("(var4 down)" 191 261)
  ("(var4 stable)" 261 290)
  ("(var1 stable)" 0 51)
  ("(var1 down)" 51 53)
  ("(var1 up)" 53 76)
  ("(var1 stable)" 76 290)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 68)
  ("(var2 stable)" 68 101)
  ("(var2 up)" 101 196)
  ("(var2 stable)" 196 290)
 )
)
(44
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 102)
  ("(var3 stable)" 102 104)
  ("(var3 up)" 104 108)
  ("(var3 stable)" 108 185)
  ("(var3 up)" 185 192)
  ("(var3 down)" 192 201)
  ("(var3 up)" 201 205)
  ("(var3 stable)" 205 341)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 106)
  ("(var4 stable)" 106 200)
  ("(var4 down)" 200 294)
  ("(var4 stable)" 294 341)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 102)
  ("(var1 down)" 102 104)
  ("(var1 up)" 104 106)
  ("(var1 stable)" 106 341)
  ("(var2 stable)" 0 95)
  ("(var2 down)" 95 99)
  ("(var2 up)" 99 134)
  ("(var2 down)" 134 136)
  ("(var2 up)" 136 217)
  ("(var2 stable)" 217 341)
 )
)
(45
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 108)
  ("(var3 stable)" 108 193)
  ("(var3 up)" 193 198)
  ("(var3 down)" 198 207)
  ("(var3 up)" 207 212)
  ("(var3 stable)" 212 348)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 111)
  ("(var4 stable)" 111 231)
  ("(var4 down)" 231 305)
  ("(var4 stable)" 305 348)
  ("(var1 stable)" 0 84)
  ("(var1 down)" 84 86)
  ("(var1 up)" 86 109)
  ("(var1 stable)" 109 348)
  ("(var2 stable)" 0 101)
  ("(var2 down)" 101 103)
  ("(var2 up)" 103 239)
  ("(var2 down)" 239 241)
  ("(var2 stable)" 241 348)
 )
)
(46
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 105)
  ("(var3 stable)" 105 182)
  ("(var3 up)" 182 187)
  ("(var3 down)" 187 196)
  ("(var3 up)" 196 202)
  ("(var3 stable)" 202 337)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 106)
  ("(var4 stable)" 106 219)
  ("(var4 down)" 219 221)
  ("(var4 stable)" 221 223)
  ("(var4 down)" 223 292)
  ("(var4 stable)" 292 295)
  ("(var4 down)" 295 297)
  ("(var4 stable)" 297 337)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 100)
  ("(var1 stable)" 100 337)
  ("(var2 stable)" 0 91)
  ("(var2 down)" 91 93)
  ("(var2 up)" 93 193)
  ("(var2 stable)" 193 195)
  ("(var2 up)" 195 227)
  ("(var2 stable)" 227 337)
 )
)
(47
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 48)
  ("(var3 up)" 48 50)
  ("(var3 down)" 50 52)
  ("(var3 up)" 52 83)
  ("(var3 stable)" 83 150)
  ("(var3 up)" 150 156)
  ("(var3 down)" 156 167)
  ("(var3 up)" 167 171)
  ("(var3 stable)" 171 298)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 78)
  ("(var4 stable)" 78 160)
  ("(var4 down)" 160 196)
  ("(var4 stable)" 196 198)
  ("(var4 down)" 198 262)
  ("(var4 stable)" 262 298)
  ("(var1 stable)" 0 54)
  ("(var1 up)" 54 77)
  ("(var1 stable)" 77 298)
  ("(var2 stable)" 0 69)
  ("(var2 down)" 69 71)
  ("(var2 up)" 71 174)
  ("(var2 stable)" 174 298)
 )
)
(48
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 120)
  ("(var3 stable)" 120 124)
  ("(var3 up)" 124 126)
  ("(var3 stable)" 126 207)
  ("(var3 up)" 207 214)
  ("(var3 down)" 214 225)
  ("(var3 up)" 225 231)
  ("(var3 stable)" 231 379)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 123)
  ("(var4 stable)" 123 220)
  ("(var4 down)" 220 222)
  ("(var4 up)" 222 224)
  ("(var4 stable)" 224 260)
  ("(var4 down)" 260 332)
  ("(var4 up)" 332 334)
  ("(var4 down)" 334 361)
  ("(var4 stable)" 361 379)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 96)
  ("(var1 down)" 96 98)
  ("(var1 up)" 98 114)
  ("(var1 down)" 114 116)
  ("(var1 stable)" 116 379)
  ("(var2 stable)" 0 112)
  ("(var2 down)" 112 114)
  ("(var2 up)" 114 234)
  ("(var2 stable)" 234 379)
 )
)
(49
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 82)
  ("(var3 stable)" 82 161)
  ("(var3 up)" 161 165)
  ("(var3 stable)" 165 167)
  ("(var3 down)" 167 175)
  ("(var3 up)" 175 179)
  ("(var3 stable)" 179 316)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 49)
  ("(var4 stable)" 49 51)
  ("(var4 up)" 51 87)
  ("(var4 stable)" 87 175)
  ("(var4 down)" 175 298)
  ("(var4 stable)" 298 316)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 75)
  ("(var1 stable)" 75 77)
  ("(var1 up)" 77 79)
  ("(var1 stable)" 79 316)
  ("(var2 stable)" 0 70)
  ("(var2 down)" 70 72)
  ("(var2 stable)" 72 104)
  ("(var2 up)" 104 106)
  ("(var2 down)" 106 108)
  ("(var2 up)" 108 189)
  ("(var2 stable)" 189 316)
 )
)
(50
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 99)
  ("(var3 stable)" 99 181)
  ("(var3 up)" 181 185)
  ("(var3 down)" 185 195)
  ("(var3 up)" 195 200)
  ("(var3 stable)" 200 335)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 98)
  ("(var4 down)" 98 100)
  ("(var4 stable)" 100 215)
  ("(var4 down)" 215 217)
  ("(var4 stable)" 217 220)
  ("(var4 down)" 220 292)
  ("(var4 stable)" 292 335)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 97)
  ("(var1 stable)" 97 335)
  ("(var2 stable)" 0 88)
  ("(var2 down)" 88 90)
  ("(var2 stable)" 90 127)
  ("(var2 up)" 127 226)
  ("(var2 stable)" 226 335)
 )
)
(51
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 115)
  ("(var3 stable)" 115 198)
  ("(var3 down)" 198 200)
  ("(var3 up)" 200 204)
  ("(var3 down)" 204 215)
  ("(var3 stable)" 215 217)
  ("(var3 up)" 217 222)
  ("(var3 stable)" 222 363)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 121)
  ("(var4 stable)" 121 215)
  ("(var4 down)" 215 218)
  ("(var4 stable)" 218 220)
  ("(var4 down)" 220 222)
  ("(var4 up)" 222 225)
  ("(var4 down)" 225 312)
  ("(var4 up)" 312 314)
  ("(var4 down)" 314 316)
  ("(var4 stable)" 316 363)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 111)
  ("(var1 stable)" 111 363)
  ("(var2 stable)" 0 104)
  ("(var2 down)" 104 109)
  ("(var2 up)" 109 237)
  ("(var2 down)" 237 239)
  ("(var2 up)" 239 242)
  ("(var2 stable)" 242 363)
 )
)
(52
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 58)
  ("(var3 stable)" 58 60)
  ("(var3 up)" 60 90)
  ("(var3 stable)" 90 163)
  ("(var3 up)" 163 167)
  ("(var3 down)" 167 178)
  ("(var3 up)" 178 183)
  ("(var3 stable)" 183 317)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 82)
  ("(var4 down)" 82 84)
  ("(var4 stable)" 84 178)
  ("(var4 down)" 178 180)
  ("(var4 up)" 180 182)
  ("(var4 down)" 182 185)
  ("(var4 up)" 185 187)
  ("(var4 down)" 187 289)
  ("(var4 stable)" 289 317)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 79)
  ("(var1 stable)" 79 317)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 stable)" 74 108)
  ("(var2 up)" 108 201)
  ("(var2 stable)" 201 317)
 )
)
(53
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 51)
  ("(var3 down)" 51 53)
  ("(var3 up)" 53 79)
  ("(var3 stable)" 79 82)
  ("(var3 up)" 82 84)
  ("(var3 stable)" 84 159)
  ("(var3 up)" 159 163)
  ("(var3 down)" 163 173)
  ("(var3 up)" 173 178)
  ("(var3 down)" 178 180)
  ("(var3 stable)" 180 311)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 84)
  ("(var4 stable)" 84 182)
  ("(var4 down)" 182 264)
  ("(var4 stable)" 264 309)
  ("(var4 up)" 309 311)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 75)
  ("(var1 stable)" 75 311)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 206)
  ("(var2 stable)" 206 311)
 )
)
(54
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 111)
  ("(var3 stable)" 111 191)
  ("(var3 up)" 191 195)
  ("(var3 down)" 195 205)
  ("(var3 up)" 205 212)
  ("(var3 stable)" 212 342)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 112)
  ("(var4 stable)" 112 193)
  ("(var4 up)" 193 195)
  ("(var4 down)" 195 197)
  ("(var4 up)" 197 199)
  ("(var4 stable)" 199 233)
  ("(var4 down)" 233 301)
  ("(var4 stable)" 301 342)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 84)
  ("(var1 stable)" 84 86)
  ("(var1 up)" 86 105)
  ("(var1 down)" 105 107)
  ("(var1 stable)" 107 342)
  ("(var2 stable)" 0 100)
  ("(var2 down)" 100 102)
  ("(var2 up)" 102 217)
  ("(var2 stable)" 217 342)
 )
)
(55
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 82)
  ("(var3 stable)" 82 163)
  ("(var3 up)" 163 168)
  ("(var3 down)" 168 179)
  ("(var3 up)" 179 184)
  ("(var3 stable)" 184 320)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 55)
  ("(var4 down)" 55 57)
  ("(var4 up)" 57 93)
  ("(var4 stable)" 93 170)
  ("(var4 down)" 170 210)
  ("(var4 up)" 210 212)
  ("(var4 down)" 212 278)
  ("(var4 stable)" 278 320)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 80)
  ("(var1 stable)" 80 320)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 stable)" 73 111)
  ("(var2 up)" 111 116)
  ("(var2 down)" 116 118)
  ("(var2 up)" 118 199)
  ("(var2 down)" 199 201)
  ("(var2 up)" 201 205)
  ("(var2 stable)" 205 320)
 )
)
(56
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 100)
  ("(var3 stable)" 100 173)
  ("(var3 up)" 173 180)
  ("(var3 down)" 180 189)
  ("(var3 stable)" 189 191)
  ("(var3 up)" 191 196)
  ("(var3 stable)" 196 326)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 98)
  ("(var4 stable)" 98 182)
  ("(var4 up)" 182 184)
  ("(var4 down)" 184 283)
  ("(var4 stable)" 283 326)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 90)
  ("(var1 stable)" 90 326)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 89)
  ("(var2 stable)" 89 104)
  ("(var2 up)" 104 204)
  ("(var2 stable)" 204 326)
 )
)
(57
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 109)
  ("(var3 down)" 109 111)
  ("(var3 up)" 111 113)
  ("(var3 stable)" 113 196)
  ("(var3 up)" 196 200)
  ("(var3 down)" 200 210)
  ("(var3 up)" 210 214)
  ("(var3 stable)" 214 350)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 114)
  ("(var4 down)" 114 116)
  ("(var4 up)" 116 118)
  ("(var4 stable)" 118 206)
  ("(var4 down)" 206 306)
  ("(var4 stable)" 306 348)
  ("(var4 down)" 348 350)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 113)
  ("(var1 stable)" 113 350)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 104)
  ("(var2 up)" 104 244)
  ("(var2 stable)" 244 350)
 )
)
(58
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 91)
  ("(var3 stable)" 91 170)
  ("(var3 up)" 170 173)
  ("(var3 stable)" 173 175)
  ("(var3 down)" 175 186)
  ("(var3 up)" 186 197)
  ("(var3 stable)" 197 339)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 46)
  ("(var4 down)" 46 48)
  ("(var4 up)" 48 83)
  ("(var4 stable)" 83 85)
  ("(var4 up)" 85 87)
  ("(var4 stable)" 87 204)
  ("(var4 down)" 204 301)
  ("(var4 stable)" 301 339)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 62)
  ("(var1 stable)" 62 64)
  ("(var1 up)" 64 80)
  ("(var1 stable)" 80 339)
  ("(var2 stable)" 0 70)
  ("(var2 down)" 70 72)
  ("(var2 stable)" 72 110)
  ("(var2 up)" 110 112)
  ("(var2 stable)" 112 114)
  ("(var2 up)" 114 176)
  ("(var2 stable)" 176 178)
  ("(var2 up)" 178 217)
  ("(var2 stable)" 217 339)
 )
)
(59
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 82)
  ("(var3 stable)" 82 171)
  ("(var3 up)" 171 176)
  ("(var3 down)" 176 186)
  ("(var3 up)" 186 192)
  ("(var3 stable)" 192 338)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 83)
  ("(var4 stable)" 83 180)
  ("(var4 down)" 180 217)
  ("(var4 stable)" 217 219)
  ("(var4 down)" 219 282)
  ("(var4 up)" 282 284)
  ("(var4 down)" 284 291)
  ("(var4 stable)" 291 338)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 79)
  ("(var1 stable)" 79 338)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 75)
  ("(var2 stable)" 75 112)
  ("(var2 up)" 112 114)
  ("(var2 stable)" 114 116)
  ("(var2 up)" 116 196)
  ("(var2 stable)" 196 338)
 )
)
(60
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 74)
  ("(var3 stable)" 74 149)
  ("(var3 up)" 149 154)
  ("(var3 down)" 154 164)
  ("(var3 up)" 164 167)
  ("(var3 stable)" 167 299)
  ("(var4 stable)" 0 38)
  ("(var4 down)" 38 40)
  ("(var4 up)" 40 73)
  ("(var4 stable)" 73 155)
  ("(var4 down)" 155 189)
  ("(var4 stable)" 189 191)
  ("(var4 down)" 191 256)
  ("(var4 stable)" 256 299)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 68)
  ("(var1 stable)" 68 299)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 60)
  ("(var2 up)" 60 184)
  ("(var2 stable)" 184 299)
 )
)
(61
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 100)
  ("(var3 stable)" 100 181)
  ("(var3 up)" 181 187)
  ("(var3 stable)" 187 189)
  ("(var3 down)" 189 198)
  ("(var3 up)" 198 206)
  ("(var3 stable)" 206 348)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 67)
  ("(var4 stable)" 67 69)
  ("(var4 up)" 69 110)
  ("(var4 stable)" 110 228)
  ("(var4 down)" 228 304)
  ("(var4 stable)" 304 348)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 98)
  ("(var1 stable)" 98 348)
  ("(var2 stable)" 0 88)
  ("(var2 down)" 88 90)
  ("(var2 up)" 90 228)
  ("(var2 stable)" 228 348)
 )
)
(62
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 100)
  ("(var3 down)" 100 102)
  ("(var3 up)" 102 104)
  ("(var3 stable)" 104 180)
  ("(var3 up)" 180 185)
  ("(var3 down)" 185 192)
  ("(var3 stable)" 192 194)
  ("(var3 up)" 194 199)
  ("(var3 stable)" 199 329)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 116)
  ("(var4 down)" 116 119)
  ("(var4 stable)" 119 204)
  ("(var4 down)" 204 285)
  ("(var4 stable)" 285 325)
  ("(var4 down)" 325 327)
  ("(var4 stable)" 327 329)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 102)
  ("(var1 stable)" 102 329)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 stable)" 98 130)
  ("(var2 up)" 130 230)
  ("(var2 stable)" 230 329)
 )
)
(63
 (
  ("(var3 stable)" 0 30)
  ("(var3 up)" 30 32)
  ("(var3 stable)" 32 34)
  ("(var3 up)" 34 61)
  ("(var3 stable)" 61 133)
  ("(var3 up)" 133 135)
  ("(var3 down)" 135 147)
  ("(var3 up)" 147 151)
  ("(var3 stable)" 151 276)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 61)
  ("(var4 stable)" 61 144)
  ("(var4 down)" 144 177)
  ("(var4 up)" 177 179)
  ("(var4 down)" 179 237)
  ("(var4 stable)" 237 276)
  ("(var1 stable)" 0 27)
  ("(var1 up)" 27 58)
  ("(var1 stable)" 58 276)
  ("(var2 stable)" 0 49)
  ("(var2 down)" 49 51)
  ("(var2 up)" 51 170)
  ("(var2 stable)" 170 276)
 )
)
(64
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 88)
  ("(var3 stable)" 88 163)
  ("(var3 up)" 163 167)
  ("(var3 down)" 167 176)
  ("(var3 up)" 176 182)
  ("(var3 stable)" 182 314)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 83)
  ("(var4 stable)" 83 195)
  ("(var4 down)" 195 197)
  ("(var4 stable)" 197 199)
  ("(var4 down)" 199 275)
  ("(var4 stable)" 275 314)
  ("(var1 stable)" 0 59)
  ("(var1 down)" 59 61)
  ("(var1 up)" 61 79)
  ("(var1 stable)" 79 314)
  ("(var2 stable)" 0 74)
  ("(var2 down)" 74 76)
  ("(var2 up)" 76 169)
  ("(var2 down)" 169 171)
  ("(var2 up)" 171 198)
  ("(var2 stable)" 198 314)
 )
)
(65
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 88)
  ("(var3 stable)" 88 158)
  ("(var3 up)" 158 162)
  ("(var3 down)" 162 172)
  ("(var3 up)" 172 178)
  ("(var3 stable)" 178 310)
  ("(var4 up)" 0 2)
  ("(var4 down)" 2 4)
  ("(var4 up)" 4 7)
  ("(var4 down)" 7 10)
  ("(var4 stable)" 10 41)
  ("(var4 up)" 41 84)
  ("(var4 stable)" 84 180)
  ("(var4 up)" 180 183)
  ("(var4 down)" 183 269)
  ("(var4 stable)" 269 310)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 57)
  ("(var1 up)" 57 74)
  ("(var1 down)" 74 76)
  ("(var1 stable)" 76 310)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 194)
  ("(var2 stable)" 194 310)
 )
)
(66
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 121)
  ("(var3 stable)" 121 191)
  ("(var3 up)" 191 196)
  ("(var3 down)" 196 207)
  ("(var3 up)" 207 211)
  ("(var3 stable)" 211 341)
  ("(var4 stable)" 0 88)
  ("(var4 up)" 88 130)
  ("(var4 stable)" 130 217)
  ("(var4 down)" 217 298)
  ("(var4 stable)" 298 341)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 92)
  ("(var1 stable)" 92 94)
  ("(var1 up)" 94 114)
  ("(var1 stable)" 114 341)
  ("(var2 stable)" 0 105)
  ("(var2 down)" 105 107)
  ("(var2 stable)" 107 142)
  ("(var2 up)" 142 149)
  ("(var2 down)" 149 151)
  ("(var2 up)" 151 232)
  ("(var2 down)" 232 234)
  ("(var2 up)" 234 239)
  ("(var2 stable)" 239 341)
 )
)
(67
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 105)
  ("(var3 stable)" 105 108)
  ("(var3 up)" 108 112)
  ("(var3 stable)" 112 183)
  ("(var3 up)" 183 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 205)
  ("(var3 stable)" 205 333)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 74)
  ("(var4 stable)" 74 77)
  ("(var4 up)" 77 109)
  ("(var4 stable)" 109 205)
  ("(var4 down)" 205 300)
  ("(var4 stable)" 300 333)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 105)
  ("(var1 stable)" 105 333)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 up)" 98 220)
  ("(var2 stable)" 220 333)
 )
)
(68
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 95)
  ("(var3 stable)" 95 170)
  ("(var3 up)" 170 175)
  ("(var3 down)" 175 185)
  ("(var3 up)" 185 190)
  ("(var3 stable)" 190 322)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 90)
  ("(var4 stable)" 90 200)
  ("(var4 down)" 200 285)
  ("(var4 stable)" 285 322)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 86)
  ("(var1 stable)" 86 322)
  ("(var2 stable)" 0 80)
  ("(var2 down)" 80 82)
  ("(var2 up)" 82 203)
  ("(var2 stable)" 203 322)
 )
)
(69
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 94)
  ("(var3 stable)" 94 96)
  ("(var3 up)" 96 98)
  ("(var3 stable)" 98 176)
  ("(var3 up)" 176 181)
  ("(var3 down)" 181 190)
  ("(var3 stable)" 190 192)
  ("(var3 up)" 192 196)
  ("(var3 stable)" 196 330)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 73)
  ("(var4 stable)" 73 75)
  ("(var4 up)" 75 101)
  ("(var4 stable)" 101 103)
  ("(var4 up)" 103 105)
  ("(var4 stable)" 105 201)
  ("(var4 down)" 201 298)
  ("(var4 stable)" 298 330)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 100)
  ("(var1 stable)" 100 330)
  ("(var2 stable)" 0 90)
  ("(var2 down)" 90 92)
  ("(var2 stable)" 92 126)
  ("(var2 up)" 126 215)
  ("(var2 stable)" 215 330)
 )
)
(70
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 66)
  ("(var3 stable)" 66 147)
  ("(var3 up)" 147 150)
  ("(var3 down)" 150 160)
  ("(var3 up)" 160 167)
  ("(var3 stable)" 167 296)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 67)
  ("(var4 stable)" 67 172)
  ("(var4 down)" 172 256)
  ("(var4 stable)" 256 296)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 61)
  ("(var1 stable)" 61 296)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 60)
  ("(var2 stable)" 60 86)
  ("(var2 up)" 86 90)
  ("(var2 stable)" 90 93)
  ("(var2 up)" 93 183)
  ("(var2 stable)" 183 296)
 )
)
(71
 (
  ("(var3 stable)" 0 53)
  ("(var3 down)" 53 55)
  ("(var3 up)" 55 88)
  ("(var3 stable)" 88 162)
  ("(var3 up)" 162 167)
  ("(var3 down)" 167 177)
  ("(var3 up)" 177 179)
  ("(var3 stable)" 179 315)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 89)
  ("(var4 stable)" 89 176)
  ("(var4 down)" 176 178)
  ("(var4 up)" 178 180)
  ("(var4 down)" 180 184)
  ("(var4 up)" 184 186)
  ("(var4 down)" 186 278)
  ("(var4 stable)" 278 315)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 79)
  ("(var1 stable)" 79 315)
  ("(var2 stable)" 0 73)
  ("(var2 down)" 73 75)
  ("(var2 stable)" 75 108)
  ("(var2 up)" 108 115)
  ("(var2 stable)" 115 117)
  ("(var2 up)" 117 207)
  ("(var2 stable)" 207 315)
 )
)
(72
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 40)
  ("(var3 stable)" 40 44)
  ("(var3 up)" 44 73)
  ("(var3 stable)" 73 161)
  ("(var3 up)" 161 167)
  ("(var3 down)" 167 176)
  ("(var3 up)" 176 183)
  ("(var3 stable)" 183 333)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 41)
  ("(var4 down)" 41 44)
  ("(var4 up)" 44 75)
  ("(var4 stable)" 75 208)
  ("(var4 down)" 208 210)
  ("(var4 up)" 210 212)
  ("(var4 down)" 212 267)
  ("(var4 stable)" 267 269)
  ("(var4 down)" 269 282)
  ("(var4 stable)" 282 317)
  ("(var4 up)" 317 319)
  ("(var4 down)" 319 321)
  ("(var4 stable)" 321 333)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 79)
  ("(var1 stable)" 79 333)
  ("(var2 stable)" 0 64)
  ("(var2 down)" 64 66)
  ("(var2 stable)" 66 100)
  ("(var2 up)" 100 202)
  ("(var2 down)" 202 204)
  ("(var2 stable)" 204 333)
 )
)
(73
 (
  ("(var3 stable)" 0 32)
  ("(var3 up)" 32 83)
  ("(var3 stable)" 83 146)
  ("(var3 up)" 146 151)
  ("(var3 down)" 151 161)
  ("(var3 up)" 161 168)
  ("(var3 stable)" 168 297)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 69)
  ("(var4 stable)" 69 154)
  ("(var4 down)" 154 259)
  ("(var4 stable)" 259 297)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 61)
  ("(var1 stable)" 61 297)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 up)" 58 186)
  ("(var2 stable)" 186 297)
 )
)
(74
 (
  ("(var3 up)" 0 2)
  ("(var3 stable)" 2 58)
  ("(var3 up)" 58 90)
  ("(var3 stable)" 90 180)
  ("(var3 up)" 180 185)
  ("(var3 down)" 185 195)
  ("(var3 up)" 195 198)
  ("(var3 stable)" 198 349)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 66)
  ("(var4 stable)" 66 68)
  ("(var4 up)" 68 93)
  ("(var4 stable)" 93 194)
  ("(var4 down)" 194 291)
  ("(var4 up)" 291 293)
  ("(var4 down)" 293 295)
  ("(var4 stable)" 295 298)
  ("(var4 down)" 298 302)
  ("(var4 up)" 302 304)
  ("(var4 down)" 304 306)
  ("(var4 up)" 306 309)
  ("(var4 down)" 309 311)
  ("(var4 stable)" 311 349)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 85)
  ("(var1 stable)" 85 88)
  ("(var1 up)" 88 91)
  ("(var1 stable)" 91 349)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 88)
  ("(var2 up)" 88 233)
  ("(var2 stable)" 233 235)
  ("(var2 up)" 235 237)
  ("(var2 stable)" 237 349)
 )
)
(75
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 107)
  ("(var3 stable)" 107 188)
  ("(var3 up)" 188 193)
  ("(var3 down)" 193 204)
  ("(var3 up)" 204 208)
  ("(var3 stable)" 208 347)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 106)
  ("(var4 stable)" 106 227)
  ("(var4 down)" 227 233)
  ("(var4 up)" 233 235)
  ("(var4 down)" 235 302)
  ("(var4 stable)" 302 347)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 84)
  ("(var1 down)" 84 86)
  ("(var1 up)" 86 106)
  ("(var1 stable)" 106 347)
  ("(var2 stable)" 0 95)
  ("(var2 down)" 95 97)
  ("(var2 up)" 97 143)
  ("(var2 down)" 143 145)
  ("(var2 up)" 145 217)
  ("(var2 stable)" 217 347)
 )
)
(76
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 59)
  ("(var3 stable)" 59 61)
  ("(var3 up)" 61 88)
  ("(var3 stable)" 88 166)
  ("(var3 up)" 166 169)
  ("(var3 stable)" 169 171)
  ("(var3 down)" 171 180)
  ("(var3 up)" 180 185)
  ("(var3 stable)" 185 315)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 97)
  ("(var4 stable)" 97 182)
  ("(var4 down)" 182 270)
  ("(var4 up)" 270 272)
  ("(var4 down)" 272 281)
  ("(var4 stable)" 281 315)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 82)
  ("(var1 stable)" 82 315)
  ("(var2 stable)" 0 77)
  ("(var2 down)" 77 81)
  ("(var2 up)" 81 181)
  ("(var2 down)" 181 183)
  ("(var2 stable)" 183 315)
 )
)
(77
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 111)
  ("(var3 stable)" 111 186)
  ("(var3 up)" 186 190)
  ("(var3 down)" 190 201)
  ("(var3 up)" 201 204)
  ("(var3 stable)" 204 336)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 112)
  ("(var4 down)" 112 114)
  ("(var4 stable)" 114 223)
  ("(var4 down)" 223 306)
  ("(var4 stable)" 306 336)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 108)
  ("(var1 stable)" 108 336)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 99)
  ("(var2 stable)" 99 134)
  ("(var2 up)" 134 228)
  ("(var2 down)" 228 231)
  ("(var2 up)" 231 234)
  ("(var2 stable)" 234 336)
 )
)
(78
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 72)
  ("(var3 stable)" 72 154)
  ("(var3 up)" 154 158)
  ("(var3 down)" 158 168)
  ("(var3 up)" 168 174)
  ("(var3 stable)" 174 308)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 76)
  ("(var4 stable)" 76 166)
  ("(var4 down)" 166 168)
  ("(var4 stable)" 168 175)
  ("(var4 down)" 175 272)
  ("(var4 stable)" 272 308)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 73)
  ("(var1 stable)" 73 308)
  ("(var2 stable)" 0 62)
  ("(var2 down)" 62 64)
  ("(var2 up)" 64 187)
  ("(var2 stable)" 187 308)
 )
)
(79
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 86)
  ("(var3 down)" 86 88)
  ("(var3 up)" 88 118)
  ("(var3 stable)" 118 202)
  ("(var3 up)" 202 211)
  ("(var3 down)" 211 220)
  ("(var3 up)" 220 224)
  ("(var3 stable)" 224 375)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 91)
  ("(var4 stable)" 91 93)
  ("(var4 up)" 93 118)
  ("(var4 stable)" 118 221)
  ("(var4 down)" 221 317)
  ("(var4 stable)" 317 319)
  ("(var4 down)" 319 321)
  ("(var4 stable)" 321 375)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 118)
  ("(var1 stable)" 118 375)
  ("(var2 stable)" 0 108)
  ("(var2 down)" 108 110)
  ("(var2 up)" 110 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 240)
  ("(var2 stable)" 240 375)
 )
)
(80
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 107)
  ("(var3 stable)" 107 183)
  ("(var3 up)" 183 187)
  ("(var3 down)" 187 198)
  ("(var3 up)" 198 202)
  ("(var3 stable)" 202 326)
  ("(var3 down)" 326 328)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 103)
  ("(var4 stable)" 103 216)
  ("(var4 down)" 216 283)
  ("(var4 stable)" 283 328)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 95)
  ("(var1 down)" 95 97)
  ("(var1 stable)" 97 328)
  ("(var2 stable)" 0 93)
  ("(var2 down)" 93 95)
  ("(var2 up)" 95 227)
  ("(var2 stable)" 227 328)
 )
)
(81
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 95)
  ("(var3 stable)" 95 97)
  ("(var3 up)" 97 99)
  ("(var3 down)" 99 101)
  ("(var3 up)" 101 103)
  ("(var3 stable)" 103 183)
  ("(var3 up)" 183 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 202)
  ("(var3 stable)" 202 340)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 103)
  ("(var4 stable)" 103 227)
  ("(var4 down)" 227 306)
  ("(var4 stable)" 306 340)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 93)
  ("(var1 stable)" 93 95)
  ("(var1 up)" 95 97)
  ("(var1 stable)" 97 340)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 87)
  ("(var2 stable)" 87 120)
  ("(var2 up)" 120 223)
  ("(var2 stable)" 223 340)
 )
)
(82
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 89)
  ("(var3 stable)" 89 164)
  ("(var3 up)" 164 168)
  ("(var3 stable)" 168 170)
  ("(var3 down)" 170 179)
  ("(var3 up)" 179 184)
  ("(var3 stable)" 184 314)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 89)
  ("(var4 stable)" 89 206)
  ("(var4 down)" 206 277)
  ("(var4 stable)" 277 314)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 83)
  ("(var1 stable)" 83 85)
  ("(var1 up)" 85 88)
  ("(var1 stable)" 88 314)
  ("(var2 stable)" 0 77)
  ("(var2 down)" 77 79)
  ("(var2 up)" 79 192)
  ("(var2 stable)" 192 314)
 )
)
(83
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 126)
  ("(var3 stable)" 126 203)
  ("(var3 up)" 203 209)
  ("(var3 down)" 209 219)
  ("(var3 up)" 219 223)
  ("(var3 stable)" 223 361)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 93)
  ("(var4 stable)" 93 96)
  ("(var4 up)" 96 126)
  ("(var4 stable)" 126 223)
  ("(var4 down)" 223 311)
  ("(var4 stable)" 311 361)
  ("(var1 stable)" 0 97)
  ("(var1 up)" 97 123)
  ("(var1 stable)" 123 361)
  ("(var2 stable)" 0 113)
  ("(var2 down)" 113 115)
  ("(var2 up)" 115 234)
  ("(var2 stable)" 234 361)
 )
)
(84
 (
  ("(var3 stable)" 0 31)
  ("(var3 up)" 31 62)
  ("(var3 stable)" 62 135)
  ("(var3 up)" 135 139)
  ("(var3 down)" 139 148)
  ("(var3 up)" 148 151)
  ("(var3 stable)" 151 280)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 70)
  ("(var4 stable)" 70 142)
  ("(var4 down)" 142 258)
  ("(var4 stable)" 258 280)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 56)
  ("(var1 stable)" 56 280)
  ("(var2 stable)" 0 50)
  ("(var2 down)" 50 52)
  ("(var2 up)" 52 171)
  ("(var2 stable)" 171 280)
 )
)
(85
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 114)
  ("(var3 stable)" 114 116)
  ("(var3 up)" 116 118)
  ("(var3 stable)" 118 191)
  ("(var3 up)" 191 194)
  ("(var3 stable)" 194 196)
  ("(var3 down)" 196 205)
  ("(var3 up)" 205 211)
  ("(var3 stable)" 211 333)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 115)
  ("(var4 stable)" 115 208)
  ("(var4 down)" 208 285)
  ("(var4 up)" 285 287)
  ("(var4 down)" 287 289)
  ("(var4 up)" 289 291)
  ("(var4 stable)" 291 333)
  ("(var1 stable)" 0 90)
  ("(var1 up)" 90 108)
  ("(var1 stable)" 108 333)
  ("(var2 stable)" 0 104)
  ("(var2 down)" 104 106)
  ("(var2 up)" 106 226)
  ("(var2 stable)" 226 333)
 )
)
(86
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 58)
  ("(var3 stable)" 58 60)
  ("(var3 up)" 60 87)
  ("(var3 stable)" 87 165)
  ("(var3 up)" 165 170)
  ("(var3 down)" 170 178)
  ("(var3 up)" 178 182)
  ("(var3 stable)" 182 313)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 53)
  ("(var4 stable)" 53 57)
  ("(var4 up)" 57 90)
  ("(var4 stable)" 90 202)
  ("(var4 down)" 202 288)
  ("(var4 stable)" 288 313)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 83)
  ("(var1 stable)" 83 313)
  ("(var2 stable)" 0 76)
  ("(var2 down)" 76 78)
  ("(var2 up)" 78 204)
  ("(var2 down)" 204 207)
  ("(var2 up)" 207 209)
  ("(var2 stable)" 209 313)
 )
)
(87
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 108)
  ("(var3 stable)" 108 182)
  ("(var3 up)" 182 189)
  ("(var3 stable)" 189 191)
  ("(var3 down)" 191 199)
  ("(var3 up)" 199 203)
  ("(var3 stable)" 203 336)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 107)
  ("(var4 stable)" 107 208)
  ("(var4 down)" 208 294)
  ("(var4 up)" 294 296)
  ("(var4 down)" 296 298)
  ("(var4 stable)" 298 336)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 96)
  ("(var1 stable)" 96 98)
  ("(var1 up)" 98 106)
  ("(var1 stable)" 106 336)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 up)" 98 218)
  ("(var2 stable)" 218 336)
 )
)
(88
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 73)
  ("(var3 stable)" 73 75)
  ("(var3 up)" 75 99)
  ("(var3 stable)" 99 178)
  ("(var3 up)" 178 184)
  ("(var3 down)" 184 191)
  ("(var3 stable)" 191 194)
  ("(var3 up)" 194 198)
  ("(var3 stable)" 198 324)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 100)
  ("(var4 stable)" 100 192)
  ("(var4 down)" 192 284)
  ("(var4 stable)" 284 324)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 96)
  ("(var1 stable)" 96 324)
  ("(var2 stable)" 0 91)
  ("(var2 down)" 91 93)
  ("(var2 up)" 93 221)
  ("(var2 stable)" 221 324)
 )
)
(89
 (
  ("(var3 stable)" 0 24)
  ("(var3 up)" 24 62)
  ("(var3 down)" 62 64)
  ("(var3 stable)" 64 145)
  ("(var3 up)" 145 150)
  ("(var3 down)" 150 161)
  ("(var3 up)" 161 164)
  ("(var3 stable)" 164 300)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 37)
  ("(var4 down)" 37 39)
  ("(var4 up)" 39 71)
  ("(var4 stable)" 71 156)
  ("(var4 down)" 156 257)
  ("(var4 stable)" 257 300)
  ("(var1 stable)" 0 27)
  ("(var1 up)" 27 59)
  ("(var1 stable)" 59 61)
  ("(var1 up)" 61 63)
  ("(var1 stable)" 63 300)
  ("(var2 stable)" 0 54)
  ("(var2 down)" 54 56)
  ("(var2 stable)" 56 93)
  ("(var2 up)" 93 182)
  ("(var2 down)" 182 184)
  ("(var2 stable)" 184 300)
 )
)
(90
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 68)
  ("(var3 stable)" 68 70)
  ("(var3 up)" 70 93)
  ("(var3 stable)" 93 95)
  ("(var3 up)" 95 97)
  ("(var3 stable)" 97 181)
  ("(var3 up)" 181 184)
  ("(var3 stable)" 184 186)
  ("(var3 down)" 186 195)
  ("(var3 up)" 195 202)
  ("(var3 stable)" 202 340)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 67)
  ("(var4 down)" 67 69)
  ("(var4 up)" 69 92)
  ("(var4 stable)" 92 94)
  ("(var4 up)" 94 96)
  ("(var4 stable)" 96 190)
  ("(var4 down)" 190 295)
  ("(var4 stable)" 295 297)
  ("(var4 down)" 297 299)
  ("(var4 stable)" 299 340)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 67)
  ("(var1 down)" 67 70)
  ("(var1 up)" 70 96)
  ("(var1 stable)" 96 340)
  ("(var2 stable)" 0 84)
  ("(var2 down)" 84 86)
  ("(var2 up)" 86 225)
  ("(var2 stable)" 225 340)
 )
)
(91
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 62)
  ("(var3 stable)" 62 153)
  ("(var3 up)" 153 156)
  ("(var3 down)" 156 168)
  ("(var3 up)" 168 173)
  ("(var3 stable)" 173 310)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 79)
  ("(var4 stable)" 79 173)
  ("(var4 down)" 173 262)
  ("(var4 stable)" 262 310)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 60)
  ("(var1 stable)" 60 310)
  ("(var2 stable)" 0 55)
  ("(var2 down)" 55 57)
  ("(var2 stable)" 57 94)
  ("(var2 up)" 94 192)
  ("(var2 stable)" 192 310)
 )
)
(92
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 35)
  ("(var3 down)" 35 37)
  ("(var3 up)" 37 65)
  ("(var3 stable)" 65 129)
  ("(var3 up)" 129 137)
  ("(var3 down)" 137 147)
  ("(var3 up)" 147 149)
  ("(var3 stable)" 149 273)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 63)
  ("(var4 stable)" 63 140)
  ("(var4 down)" 140 245)
  ("(var4 stable)" 245 273)
  ("(var1 stable)" 0 22)
  ("(var1 up)" 22 61)
  ("(var1 stable)" 61 273)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 up)" 55 169)
  ("(var2 down)" 169 171)
  ("(var2 up)" 171 173)
  ("(var2 stable)" 173 273)
 )
)
(93
 (
  ("(var3 stable)" 0 87)
  ("(var3 up)" 87 120)
  ("(var3 stable)" 120 198)
  ("(var3 up)" 198 203)
  ("(var3 down)" 203 213)
  ("(var3 up)" 213 218)
  ("(var3 stable)" 218 359)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 116)
  ("(var4 stable)" 116 228)
  ("(var4 down)" 228 320)
  ("(var4 stable)" 320 359)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 111)
  ("(var1 stable)" 111 359)
  ("(var2 stable)" 0 104)
  ("(var2 down)" 104 106)
  ("(var2 up)" 106 215)
  ("(var2 stable)" 215 359)
 )
)
(94
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 111)
  ("(var3 stable)" 111 183)
  ("(var3 up)" 183 189)
  ("(var3 down)" 189 198)
  ("(var3 up)" 198 203)
  ("(var3 stable)" 203 332)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 110)
  ("(var4 stable)" 110 199)
  ("(var4 down)" 199 308)
  ("(var4 stable)" 308 332)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 104)
  ("(var1 stable)" 104 332)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 196)
  ("(var2 stable)" 196 198)
  ("(var2 up)" 198 211)
  ("(var2 stable)" 211 332)
 )
)
(95
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 93)
  ("(var3 stable)" 93 174)
  ("(var3 up)" 174 177)
  ("(var3 down)" 177 188)
  ("(var3 up)" 188 192)
  ("(var3 stable)" 192 328)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 93)
  ("(var4 stable)" 93 180)
  ("(var4 down)" 180 324)
  ("(var4 stable)" 324 326)
  ("(var4 down)" 326 328)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 91)
  ("(var1 stable)" 91 328)
  ("(var2 stable)" 0 80)
  ("(var2 down)" 80 84)
  ("(var2 stable)" 84 118)
  ("(var2 up)" 118 207)
  ("(var2 down)" 207 209)
  ("(var2 stable)" 209 328)
 )
)
(96
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 83)
  ("(var3 stable)" 83 85)
  ("(var3 up)" 85 116)
  ("(var3 stable)" 116 195)
  ("(var3 up)" 195 200)
  ("(var3 down)" 200 209)
  ("(var3 up)" 209 215)
  ("(var3 stable)" 215 354)
  ("(var4 stable)" 0 74)
  ("(var4 down)" 74 76)
  ("(var4 up)" 76 120)
  ("(var4 down)" 120 122)
  ("(var4 stable)" 122 212)
  ("(var4 down)" 212 317)
  ("(var4 stable)" 317 354)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 107)
  ("(var1 stable)" 107 354)
  ("(var2 stable)" 0 101)
  ("(var2 down)" 101 103)
  ("(var2 up)" 103 245)
  ("(var2 stable)" 245 354)
 )
)
(97
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 95)
  ("(var3 stable)" 95 168)
  ("(var3 up)" 168 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 312)
  ("(var4 stable)" 0 63)
  ("(var4 down)" 63 66)
  ("(var4 up)" 66 97)
  ("(var4 stable)" 97 209)
  ("(var4 down)" 209 269)
  ("(var4 stable)" 269 312)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 91)
  ("(var1 down)" 91 93)
  ("(var1 stable)" 93 312)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 87)
  ("(var2 up)" 87 223)
  ("(var2 stable)" 223 312)
 )
)
(98
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 82)
  ("(var3 down)" 82 84)
  ("(var3 stable)" 84 136)
  ("(var3 up)" 136 140)
  ("(var3 down)" 140 148)
  ("(var3 up)" 148 152)
  ("(var3 stable)" 152 278)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 62)
  ("(var4 down)" 62 64)
  ("(var4 stable)" 64 149)
  ("(var4 down)" 149 242)
  ("(var4 stable)" 242 278)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 60)
  ("(var1 stable)" 60 278)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 up)" 55 170)
  ("(var2 down)" 170 172)
  ("(var2 stable)" 172 278)
 )
)
(99
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 77)
  ("(var3 stable)" 77 152)
  ("(var3 up)" 152 157)
  ("(var3 down)" 157 167)
  ("(var3 up)" 167 171)
  ("(var3 stable)" 171 307)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 78)
  ("(var4 stable)" 78 170)
  ("(var4 down)" 170 257)
  ("(var4 stable)" 257 307)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 68)
  ("(var1 stable)" 68 307)
  ("(var2 stable)" 0 63)
  ("(var2 down)" 63 67)
  ("(var2 up)" 67 192)
  ("(var2 down)" 192 195)
  ("(var2 up)" 195 199)
  ("(var2 stable)" 199 307)
 )
)
(100
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 67)
  ("(var3 stable)" 67 142)
  ("(var3 up)" 142 148)
  ("(var3 down)" 148 157)
  ("(var3 up)" 157 162)
  ("(var3 stable)" 162 293)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 68)
  ("(var4 stable)" 68 156)
  ("(var4 down)" 156 249)
  ("(var4 stable)" 249 293)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 62)
  ("(var1 stable)" 62 293)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 up)" 58 182)
  ("(var2 stable)" 182 293)
 )
)
